
public class PointOut extends Point{

	static /*@ spec_public @*/ int num_inst; 
	
	//Regra 7.
	//@ invariant this.sema != null ;
	
	//@ requires sem != null;
	PointOut(Semaphore sem){
		super();
		this.sema = sem;
	}
	
	//@ requires po != null && n < nexts.length && po.next != null ;
	PointOut(PointOut po) {
		super(po.next,po.sema);
		nexts[n] = po.next.getId();
	}
	
	//@requires this != null && n < nexts.length && this.next != null ;
	public Object clona() {
		return new PointOut(this);
    }
	
}
